Inference at * 1 1 1 
Iof proof for Lemma nth tl is fseg:



1. T : Type
2. L1 : T List
3. L : T List
  L1 = nth_tl(||L||;L @ L1) 

latex

 by ((((ListInd 3) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 4. u : T
C1: 5. v : T List
C1: 6. L1 = nth_tl(||v||;v @ L1)
C1:   L1 = nth_tl(||v||+1;[u / (v @ L1)])
C.

Definitions

i z j, i <z j, n+m, #$n, [car / cdr], nth_tl(n;as), ||as||, as @ bs, Type, s = t, type List